4.5. 商类型🔗

商类型 允许通过降低现有类型的命题等价的细粒度来构造新类型。具体来说，给定一个类型 A 和一个等价关系 \sim，商 A / \sim 拥有与 A 相同的元素，但每对被 \sim 相关联的元素在新类型中都被视为相等。等价性在全局范围内都被满足：Lean 的逻辑中任何事物都无法察觉两个被判等的项的不同。因此，商类型为我们构建一种不可穿透的抽象屏障提供了途径。特别是，所有从商类型出发的函数都必须证明它们满足该等价关系。

def

Quotient.{u} {α : Sort u} (s : Setoid α) : Sort u
Quotient.{u} {α : Sort u} (s : Setoid α) :
  Sort u

商类型将某一类型的命题等价关系变粗,使得由某个等价关系关联的项被视为相等。该等价关系由Setoid的一个实例给出。

从集合论的角度来看,Quotient s可以被看作是α在Setoid实例的关系s.r下的等价类的集合。来自Quotient s的函数必须证明它们满足s.r:

定义一个函数f : Quotient s → β,
提供f' : α → β
并证明对于所有x : α和y : α,有s.r x y → f' x = f' y。 Quotient.lift实现了这个操作。

主要的商操作符包括:

Quotient.mk将底层类型α的元素放入商类型中。
Quotient.lift允许从商类型定义到另一个类型的函数。
Quotient.sound断言由r关联的元素相等。
Quotient.ind用于在证明商类型时假设所有元素都是通过Quotient.mk构造的。

Quotient构建在原始商类型Quot之上,后者不需要关系是等价关系的证明。对于确实为等价关系的场景,应使用Quotient而非Quot。

只要能够证明底层类型的两个元素通过等价关系相关联，那么它们在Quotient 中就是相等的。然而，定义等价不会因使用 Quotient 而改变：两个商中的元素只有当它们本就在底层类型中定义等价时，才在商类型中定义等价。

商类型在编程中用得不多，但在数学中非常常见:

整数: 整数传统上可表示为自然数对 (n, k)，它编码整数 n - k。在这种编码下，两个整数 (n_1, k_1) 和 (n_2, k_2) 当且仅当 n_1 + k_2 = n_2 + k_1 时视为相等。
有理数: 有理数 \frac{n}{d} 可编码为 (n, d)，其中 d \neq 0。两个有理数 \frac{n_1}{d_1} 和 \frac{n_2}{d_2} 当且仅当 n_1 d_2 = n_2 d_1 时视为相等。
实数: 实数可以用柯西序列来表示，但此编码不是唯一的。利用商类型，可以让它们的差收敛到零时的柯西序列判为相等。
有限集: 有限集可以用元素列表表示。通过商类型，如果两个列表包含的元素完全相同（不用要求元素类型有判定等价或序关系），则它们视为相等。

与商类型对应的另一个选项就是直接对等价类进行推理。这种方式的劣势在于其不可“计算”：知道确有一个整数等于 5+8 当然很好，对于 5+8=13 来说，它不应是一个需要证明的定理。基于等价类集合定义函数需要依赖不可计算的经典推理原则，而商类型中的函数则是普通的可计算函数，并且还尊重等价关系。

4.5.1. 商类型的替代方案🔗

虽然 Quotient 提供了一种带有合理可计算性的方便商构造方式，但通常还可以通过其他办法定义商类型。

一般来说，当一个类型 Q 满足商的普适性质时，它被称为 A 关于等价关系 \sim 的商类型：存在一个函数 q : A \to Q，使得 \forall a, b \in A, q(a) = q(b) \iff a \sim b。

由 Quotient 形成的商只在命题等价意义下满足这一性质：被 \sim$ 相关联的 A 的元素在商类型中也是等价的，因此无法区分。然而，同一个等价类中的成员在商类型中不一定定义等价。

还有一种实现方式是：在 A 内为每个等价类选择一个唯一代表，然后将 Q 定义为 A 中的元素对，再加上它们确实是该标准代表的证明。配合一个把 A 中每个 a 都映射到其标准代表的函数，Q 就成了 A 的商类型。由于证明无关性，Q 内同一等价类代表在定义上就是定义相等的。

这种手工实现的商类型 $Q$ 往往比 Quotient 更好用。特别是，由于每个等价类由唯一标准代表表示，定义自商类型的函数再不需要证明其尊重等价关系。这样也常带来更好的计算效果（商类型下同一个元素可能有多种表现形式，而手工商类型始终规范）。最后，手工商类型是归纳类型，因此能在某些场景用作嵌套归纳类型等用途，而 Quotient 却不能。然而，并非所有商类型都能手工实现。

手工实现的商类型整数

作为Nat对实现时，根据整数所需等式，每个等价类有至少一个Nat为零的标准代表。这可表示为Lean结构：

structure Z where
  a : Nat
  b : Nat
  canonical : a = 0 ∨ b = 0

因证明无关性，该结构类型中表示相同整数的每个值已经等价。用自然数截断于零的减法自动化证明构建，包装器使Z构造更便利：

def Z.mk' (n k : Nat) : Z where
  a := n - k
  b := k - n
  canonical := byn:Natk:Nat⊢ n - k = 0 ∨ k - n = 0 omegaAll goals completed! 🐙

此构造满足整数所需等式：

theorem Z_mk'_respects_eq :
    (Z.mk' n k = Z.mk' n' k') ↔ (n + k' = n' + k) := byn:Natk:Natn':Natk':Nat⊢ Z.mk' n k = Z.mk' n' k' ↔ n + k' = n' + k
  simp [Z.mk']n:Natk:Natn':Natk':Nat⊢ n - k = n' - k' ∧ k - n = k' - n' ↔ n + k' = n' + k
  omegaAll goals completed! 🐙

为了在示例中使用此类型，添加Neg、OfNat和ToString实例较便利。这些实例使示例读写更易。

instance : Neg Z where
  neg n := Z.mk' n.b n.a

instance : OfNat Z n where
  ofNat := Z.mk' n 0

instance : ToString Z where
  toString n :=
    if n.a = 0 then
      if n.b = 0 then "0"
      else s!"-{n.b}"
    else toString n.a

5#eval (5 : Z)

-5#eval (-5 : Z)

-5

加法是底层Nat的加法：

instance : Add Z where
  add n k := Z.mk' (n.a + k.a) (n.b + k.b)

17#eval (-5 + 22: Z)

由于每个等价类都唯一表示，自该类型出发的函数无需再证明符合等价关系。不过，实际开发中，建议为手动实现的商类型补齐商类型 API 以及相关的普遍性质证明。

内建整数类型作为商类型

Lean 内建的整数类型 Int 满足商类型的普遍性质，可以看作是 Nat 对的商类型。每个等价类的代表元可以通过比较和减法计算得出：标准库中该函数叫 Int.subNatNat。

def toInt (n k : Nat) : Int :=
  if n < k then - (k - n : Nat)
  else if n = k then 0
  else (n - k : Nat)

它满足商类型的普遍性质。两个 Nat 对只有在 toInt 计算结果相等时代表同一个整数：

theorem toInt_sound :
    n + k' = k + n' ↔
    toInt n k = toInt n' k' := byn:Natk':Natk:Natn':Nat⊢ n + k' = k + n' ↔ toInt n k = toInt n' k'
  simp only [toInt]n:Natk':Natk:Natn':Nat⊢ n + k' = k + n' ↔
  (if n < k then -↑(k - n) else if n = k then 0 else ↑(n - k)) =
    if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')
  splitisTruen:Natk':Natk:Natn':Nath✝:n < k⊢ n + k' = k + n' ↔ -↑(k - n) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalsen:Natk':Natk:Natn':Nath✝:¬n < k⊢ n + k' = k + n' ↔ (if n = k then 0 else ↑(n - k)) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') <;>isTruen:Natk':Natk:Natn':Nath✝:n < k⊢ n + k' = k + n' ↔ -↑(k - n) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalsen:Natk':Natk:Natn':Nath✝:¬n < k⊢ n + k' = k + n' ↔ (if n = k then 0 else ↑(n - k)) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') splitisFalse.isTruen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:n = k⊢ n + k' = k + n' ↔ 0 = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalse.isFalsen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:¬n = k⊢ n + k' = k + n' ↔ ↑(n - k) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') <;>isTrue.isTruen:Natk':Natk:Natn':Nath✝¹:n < kh✝:n' < k'⊢ n + k' = k + n' ↔ -↑(k - n) = -↑(k' - n')isTrue.isFalsen:Natk':Natk:Natn':Nath✝¹:n < kh✝:¬n' < k'⊢ n + k' = k + n' ↔ -↑(k - n) = if n' = k' then 0 else ↑(n' - k')isFalse.isTruen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:n = k⊢ n + k' = k + n' ↔ 0 = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalse.isFalsen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:¬n = k⊢ n + k' = k + n' ↔ ↑(n - k) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') omegaAll goals completed! 🐙

4.5.2. 集合体（Setoid）🔗

商类型基于集合体（setoid）概念。 集合体 指一个类型和其上选定的等价关系的配对。不同于商类型，集合体并不强制抽象屏障，对等价关系的自动化证明（如简化）不能直接用集合体中的等价关系。除了作为商类型的基础结构外，集合体本身也有其用途。

type class

Setoid.{u} (α : Sort u) : Sort (max 1 u)
Setoid.{u} (α : Sort u) : Sort (max 1 u)

Setoid 是一个带有特殊等价关系(记作 ≈)的类型

Quotient 类型的构造子需要一个 Setoid 实例

Instance Constructor

Setoid.mk.{u}

Methods

r : α → α → Prop

x ≈ y 是一个集合体(setoid)的特殊等价关系。

iseqv : Equivalence ZhDoc.Setoid.r

x ≈ y 是一个等价关系。

theorem

Setoid.refl.{u} {α : Sort u} [Setoid α] (a : α) : a ≈ a
Setoid.refl.{u} {α : Sort u} [Setoid α]
  (a : α) : a ≈ a

集合体的等价关系是自反的。

theorem

Setoid.symm.{u} {α : Sort u} [Setoid α] {a b : α} (hab : a ≈ b) : b ≈ a
Setoid.symm.{u} {α : Sort u} [Setoid α]
  {a b : α} (hab : a ≈ b) : b ≈ a

集合体的等价关系是对称的。

theorem

Setoid.trans.{u} {α : Sort u} [Setoid α] {a b c : α} (hab : a ≈ b)
  (hbc : b ≈ c) : a ≈ c
Setoid.trans.{u} {α : Sort u} [Setoid α]
  {a b c : α} (hab : a ≈ b)
  (hbc : b ≈ c) : a ≈ c

集合体的等价关系是对称的。

4.5.3. 等价关系🔗

等价关系 指的是自反、对称且传递的关系。

syntax等价关系

某个类型上的“标准”等价关系记为 ≈，它是通过类型类 HasEquiv 重载的。

term ::= ...
    | `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`.term ≈ term

type class

HasEquiv.{u, v} (α : Sort u) : Sort (max u (v + 1))
HasEquiv.{u, v} (α : Sort u) :
  Sort (max u (v + 1))

HasEquiv α是一个类型类,它支持记号x ≈ y,其中x y : α.

Instance Constructor

HasEquiv.mk.{u, v}

Methods

Equiv : α → α → Sort v

``x ≈ y表示x和y`是等价的。由于这是一个类型类，等价的概念取决于类型。

声明某关系 r 实际上是等价关系用 Equivalence r 实现。

structure

Equivalence.{u} {α : Sort u} (r : α → α → Prop) : Prop
Equivalence.{u} {α : Sort u}
  (r : α → α → Prop) : Prop

一个等价关系 r: α → α → Prop 是满足以下条件的关系:

自反性: r x x,
对称性: r x y 蕴含 r y x, 并且
传递性: r x y 且 r y z 蕴含 r x z.

相等关系是一个等价关系, 并且等价关系具有许多与相等关系类似的性质。

Constructor

Equivalence.mk.{u}

Fields

refl : ∀ (x : α), r x x

等价关系具有自反性: r x x

symm : ∀ {x y : α}, r x y → r y x

等价关系具有对称性: r x y 蕴含 r y x

trans : ∀ {x y z : α}, r x y → r y z → r x z

等价关系具有传递性: r x y 和 r y z 蕴含 r x z

每一个 Setoid 实例都自动带来一个对应的 HasEquiv 实例：

4.5.4. 商类型 API🔗

商类型 API 依赖已存在的 Setoid 实例。

4.5.4.1. 构造商类型🔗

Quotient 类型需要以普通参数形式显式传入 Setoid 实例（而不是作为隐式实例参数）。这样可以保证商类型使用的是期望的等价关系。该实例可通过取名或用 inferInstance 获得。

商类型中的值实际上就是集合体的底层类型的元素, 用 Quotient.mk 包裹。

def

Quotient.mk.{u} {α : Sort u} (s : Setoid α) (a : α) : Quotient s
Quotient.mk.{u} {α : Sort u}
  (s : Setoid α) (a : α) : Quotient s

把某个类型的元素放入商类型中,该商类型根据等价关系将元素进行等价。

setoid 实例需要显式提供。而 Quotient.mk' 使用了实例合成。

给定 v : α, Quotient.mk s v : Quotient s 类似于 v, 只是对 v 值都必须满足 s.r。 Quotient.lift 允许将商类型中的值映射到其他类型,只要这种映射遵循 s.r。

def

Quotient.mk'.{u} {α : Sort u} [s : Setoid α] (a : α) : Quotient s
Quotient.mk'.{u} {α : Sort u}
  [s : Setoid α] (a : α) : Quotient s

将某个类型的元素放入通过等价关系对项进行等价分类的商类型中。

等价关系是通过合成一个Setoid实例来找到的。Quotient.mk则要求显式地提供该实例。

给定v : α，Quotient.mk' v : Quotient s就像是v，只不过对v值的必须满足s.r。 Quotient.lift允许将商集中的值映射到其他类型，只要该映射满足s.r即可。

用商类型定义整数

整数可定义为一对自然数，并通过它们的差值来表示。该表示不是唯一的，比如 (4, 7) 和 (1, 4) 都表示 -3。

两个整数编码在何时相等由 Z.eq 决定：

def Z' : Type := Nat × Nat

def Z.eq (n k : Z') : Prop :=
  n.1 + k.2 = n.2 + k.1

该关系是个等价关系：

def Z.eq.eqv : Equivalence Z.eq where
  refl := by⊢ ∀ (x : Z'), eq x x
    intro (x, y)x:Naty:Nat⊢ eq (x, y) (x, y)
    simp +arith [eq]All goals completed! 🐙
  symm := by⊢ ∀ {x y : Z'}, eq x y → eq y x
    intro (x, y) (x', y') heqx:Naty:Natx':Naty':Natheq:eq (x, y) (x', y')⊢ eq (x', y') (x, y)
    simp_all only [eq]x:Naty:Natx':Naty':Natheq:x + y' = y + x'⊢ x' + y = y' + x
    omegaAll goals completed! 🐙
  trans := by⊢ ∀ {x y z : Z'}, eq x y → eq y z → eq x z
    intro (x, y) (x', y') (x'', y'')x:Naty:Natx':Naty':Natx'':Naty'':Nat⊢ eq (x, y) (x', y') → eq (x', y') (x'', y'') → eq (x, y) (x'', y'')
    intro heq1 heq2x:Naty:Natx':Naty':Natx'':Naty'':Natheq1:eq (x, y) (x', y')heq2:eq (x', y') (x'', y'')⊢ eq (x, y) (x'', y'')
    simp_all only [eq]x:Naty:Natx':Naty':Natx'':Naty'':Natheq1:x + y' = y + x'heq2:x' + y'' = y' + x''⊢ x + y'' = y + x''
    omegaAll goals completed! 🐙

可以据此实现 Setoid 实例：

instance Z.instSetoid : Setoid Z' where
  r := Z.eq
  iseqv := Z.eq.eqv

于是类型 Z 是 Z' 在此 Setoid 实例下的商类型：

def Z : Type := Quotient Z.instSetoid

可用辅助函数 Z.mk 省去每次显式传递实例的麻烦：

def Z.mk (n : Z') : Z := Quotient.mk _ n

当然，数值字面量更方便。给出 OfNat 实例可让整数接受数字字面量：

instance : OfNat Z n where
  ofNat := Z.mk (n, 0)

4.5.4.2. 消解商类型🔗

要从商类型出发定义函数，只需证明相应的底层函数保持等价关系。可使用 Quotient.lift 或二元版本 Quotient.lift₂ 实现。变体 Quotient.liftOn 和 Quotient.liftOn₂ 则是将商类型实参放在参数列表前。

def

Quotient.lift.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α}
  (f : α → β) : (∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β
Quotient.lift.{u, v} {α : Sort u}
  {β : Sort v} {s : Setoid α}
  (f : α → β) :
  (∀ (a b : α), a ≈ b → f a = f b) →
    Quotient s → β

将一个函数从底层类型提升为商类型的函数，要求该函数满足商类型的等价关系。

给定s : Setoid α和一个商类型Quotient s，应用一个函数f : α → β需要一个证明h，表明f满足等价关系s.r。在这种情况下，函数Quotient.lift f h : Quotient s → β的计算结果与f一致。

Quotient.liftOn是该操作的一个变体，它将商类型的值作为第一个显式参数。

def

Quotient.liftOn.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α}
  (q : Quotient s) (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) : β
Quotient.liftOn.{u, v} {α : Sort u}
  {β : Sort v} {s : Setoid α}
  (q : Quotient s) (f : α → β)
  (c : ∀ (a b : α), a ≈ b → f a = f b) : β

将一个函数从底层类型提升为作用于商类型的函数，要求该函数满足商类型的等价关系。

给定s : Setoid α和一个商类型值q : Quotient s，想要应用函数f : α → β，需要证明c，即f满足等价关系s.r。在这种情况下，Quotient.liftOn q f h : β这一项可以简化为将f应用于底层的α值的结果。

Quotient.lift是该操作的另一个版本，其参数中商类型值放在最后，而不是最前。

def

Quotient.lift₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ
Quotient.lift₂.{uA, uB, uC} {α : Sort uA}
  {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β}
  (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ →
        b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
  φ

将一个二元函数从底层类型提升为作用于商类型的二元函数。该函数必须同时满足两个商类型的等价关系。

Quotient.lift 是此操作针对一元函数的版本。Quotient.liftOn₂ 是接受商类型参数优先的版本。

def

Quotient.liftOn₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :
  φ
Quotient.liftOn₂.{uA, uB, uC}
  {α : Sort uA} {β : Sort uB}
  {φ : Sort uC} {s₁ : Setoid α}
  {s₂ : Setoid β} (q₁ : Quotient s₁)
  (q₂ : Quotient s₂) (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ →
        b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :
  φ

把一个二元函数从底层类型提升为作用于商类型上的二元函数。该函数必须兼容两个商类型的等价关系。

Quotient.liftOn是针对一元函数的该操作的一个版本。Quotient.lift₂是参数中商类型排在最后的版本。

整数的取负与加法

对于给定的由一对自然数编码而成的整数Z, 取负操作就是交换两分量： Given the encoding Z of integers as a quotient of pairs of natural numbers, negation can be implemented by swapping the first and second projections:

def neg' : Z' → Z
  | (x, y) => .mk (y, x)

只要证明其符合等价关系，即可用 Quotient.lift 升级为商类型上的函数：

instance : Neg Z where
  neg :=
    Quotient.lift neg' <| by⊢ ∀ (a b : Z'), a ≈ b → neg' a = neg' b
      intro n k equivn:Z'k:Z'equiv:n ≈ k⊢ neg' n = neg' k
      apply Quotient.soundan:Z'k:Z'equiv:n ≈ k⊢ (n.snd, n.fst) ≈ (k.snd, k.fst)
      simp only [· ≈ ·, Setoid.r, Z.eq] at *an:Z'k:Z'equiv:n.fst + k.snd = n.snd + k.fst⊢ n.snd + k.fst = n.fst + k.snd
      omegaAll goals completed! 🐙

类似地，Quotient.lift₂ 可定义二元运算，例如分量加法：

def add' (n k : Nat × Nat) : Z :=
  .mk (n.1 + k.1, n.2 + k.2)

用等价关系证明加法保持等价后即可“提升”：

instance : Add Z where
  add (n : Z) :=
    n.lift₂ add' <| byn:Z⊢ ∀ (a₁ : Nat × Nat) (b₁ : Z') (a₂ : Nat × Nat) (b₂ : Z'), a₁ ≈ a₂ → b₁ ≈ b₂ → add' a₁ b₁ = add' a₂ b₂
      intro n k n' k'n✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'⊢ n ≈ n' → k ≈ k' → add' n k = add' n' k'
      intro heq heq'n✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'heq:n ≈ n'heq':k ≈ k'⊢ add' n k = add' n' k'
      apply Quotient.soundan✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'heq:n ≈ n'heq':k ≈ k'⊢ (n.fst + k.fst, n.snd + k.snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd)
      cases na.mkn:Zk:Z'n':Nat × Natk':Z'heq':k ≈ k'fst✝:Natsnd✝:Natheq:(fst✝, snd✝) ≈ n'⊢ ((fst✝, snd✝).fst + k.fst, (fst✝, snd✝).snd + k.snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd); cases ka.mk.mkn:Zn':Nat × Natk':Z'fst✝¹:Natsnd✝¹:Natheq:(fst✝¹, snd✝¹) ≈ n'fst✝:Natsnd✝:Natheq':(fst✝, snd✝) ≈ k'⊢ ((fst✝¹, snd✝¹).fst + (fst✝, snd✝).fst, (fst✝¹, snd✝¹).snd + (fst✝, snd✝).snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd); cases n'a.mk.mk.mkn:Zk':Z'fst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natheq':(fst✝¹, snd✝¹) ≈ k'fst✝:Natsnd✝:Natheq:(fst✝², snd✝²) ≈ (fst✝, snd✝)⊢ ((fst✝², snd✝²).fst + (fst✝¹, snd✝¹).fst, (fst✝², snd✝²).snd + (fst✝¹, snd✝¹).snd) ≈
  ((fst✝, snd✝).fst + k'.fst, (fst✝, snd✝).snd + k'.snd); cases k'a.mk.mk.mk.mkn:Zfst✝³:Natsnd✝³:Natfst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natheq:(fst✝³, snd✝³) ≈ (fst✝¹, snd✝¹)fst✝:Natsnd✝:Natheq':(fst✝², snd✝²) ≈ (fst✝, snd✝)⊢ ((fst✝³, snd✝³).fst + (fst✝², snd✝²).fst, (fst✝³, snd✝³).snd + (fst✝², snd✝²).snd) ≈
  ((fst✝¹, snd✝¹).fst + (fst✝, snd✝).fst, (fst✝¹, snd✝¹).snd + (fst✝, snd✝).snd)
      simp_all only [· ≈ ·, Setoid.r, Z.eq]a.mk.mk.mk.mkn:Zfst✝³:Natsnd✝³:Natfst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natfst✝:Natsnd✝:Natheq:fst✝³ + snd✝¹ = snd✝³ + fst✝¹heq':fst✝² + snd✝ = snd✝² + fst✝⊢ fst✝³ + fst✝² + (snd✝¹ + snd✝) = snd✝³ + snd✝² + (fst✝¹ + fst✝)
      omegaAll goals completed! 🐙

若函数的返回类型是子单元，可用 Quotient.recOnSubsingleton 或 Quotient.recOnSubsingleton₂ 直接定义。因为目标类型的所有元素都已相等，函数自然保持等价关系。

def

Quotient.recOnSubsingleton.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))]
  (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) : motive q
Quotient.recOnSubsingleton.{u, v}
  {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  [h :
    ∀ (a : α),
      Subsingleton
        (motive (Quotient.mk s a))]
  (q : Quotient s)
  (f :
    (a : α) → motive (Quotient.mk s a)) :
  motive q

一种用于商类型上的递归或归纳原理的替代方法,当目标类型是子单元(所有元素都相等)时可以使用。

在这些情况下,证明函数满足商类型的等价关系是平凡的,因此任何函数都可以提升。

Quotient.rec没有假设目标类型是子单元。

def

Quotient.recOnSubsingleton₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB}
  {s₁ : Setoid α} {s₂ : Setoid β}
  {motive : Quotient s₁ → Quotient s₂ → Sort uC}
  [s :
    ∀ (a : α) (b : β),
      Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))]
  (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g :
    (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
  motive q₁ q₂
Quotient.recOnSubsingleton₂.{uA, uB, uC}
  {α : Sort uA} {β : Sort uB}
  {s₁ : Setoid α} {s₂ : Setoid β}
  {motive :
    Quotient s₁ → Quotient s₂ → Sort uC}
  [s :
    ∀ (a : α) (b : β),
      Subsingleton
        (motive (Quotient.mk s₁ a)
          (Quotient.mk s₂ b))]
  (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g :
    (a : α) →
      (b : β) →
        motive (Quotient.mk s₁ a)
          (Quotient.mk s₂ b)) :
  motive q₁ q₂

一种用于在商类型上定义二元运算的替代归纳或递归算子,可用于当目标类型是子单元时。

在这些情况下,证明函数满足商类型的等价关系是平凡的,因此任何函数都可以被提升。

4.5.4.3. 商类型上的证明🔗

在商类型上证明性质，主要工具是 soundness 公理和归纳原理。 soundness 公理表明，如果两个底层类型中的元素满足等价关系，则在商类型中相等。归纳原理类似于归纳类型的递归：若要证明某谓词对全部商类型元素成立，只需证明对每个 Quotient.mk 形式的元素成立即可。由于 Quotient 不是归纳类型，使用如 cases 或 induction 时需显式指定 Quotient.ind 并用 using 修饰。

theorem

Quotient.sound.{u} {α : Sort u} {s : Setoid α} {a b : α} :
  a ≈ b → Quotient.mk s a = Quotient.mk s b
Quotient.sound.{u} {α : Sort u}
  {s : Setoid α} {a b : α} :
  a ≈ b →
    Quotient.mk s a = Quotient.mk s b

商等价公理，它断言在setoid中相关的元素是相等的。

由于Quotient是建立在更低层类型Quot之上的，Quotient.sound被实现为一个定理。它源自于Quot.sound，即底层商类型Quot的正确性公理。

theorem

Quotient.ind.{u} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Prop} :
  (∀ (a : α), motive (Quotient.mk s a)) → ∀ (q : Quotient s), motive q
Quotient.ind.{u} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Prop} :
  (∀ (a : α), motive (Quotient.mk s a)) →
    ∀ (q : Quotient s), motive q

一个关于商类型的推理原则，允许关于商类型的证明假定所有的值都是通过Quotient.mk构造的。

商类型上的证明

给定前面例子中将整数定义为一个商类型，你可以使用 Quotient.ind 和 Quotient.sound 来证明取负是加法的逆元。首先，使用 Quotient.ind 可以将出现的 n 替换为 Quotient.mk 的应用。完成这一转换后，等式的左边，通过具体展开定义以及 Quotient.lift 的计算规则，可以归约为一次 Quotient.mk 的应用，即两边是定义等价的项。此时，就可以应用 Quotient.sound，这将带来一个新的目标：需要证明等式两边通过等价关系相关。这个目标可以通过 simp_arith 策略来证明。

theorem Z.add_neg_inverse (n : Z) : n  + (-n) = 0 := byn:Z⊢ n + -n = 0
  cases n using Quotient.indaa✝:Z'⊢ Quotient.mk instSetoid a✝ + -Quotient.mk instSetoid a✝ = 0
  apply Quotient.sounda.aa✝:Z'⊢ (a✝.fst + (a✝.snd, a✝.fst).fst, a✝.snd + (a✝.snd, a✝.fst).snd) ≈ (0, 0)
  simp +arith [· ≈ ·, Setoid.r, eq]All goals completed! 🐙

对于更特设的使用场景，可以使用 Quotient.rec，Quotient.recOn 和 Quotient.hrecOn 来从一个商类型到任意其他宇宙中的类型，定义依值函数。要说明一个依值函数能够遵循商类型的等价关系，需要处理这样一种情况：依值结果类型在等式两边会用不同的商类型里的值来实例化。 Quotient.rec 和 Quotient.recOn 会利用 Quotient.sound 将相关元素建立等价关系，并在等式中插入恰当的强制转换（cast）；而 Quotient.hrecOn 则使用异质等式（heterogeneous equality）。

def

Quotient.rec.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  (f : (a : α) → motive (Quotient.mk s a))
  (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) (q : Quotient s) :
  motive q
Quotient.rec.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (f : (a : α) → motive (Quotient.mk s a))
  (h :
    ∀ (a b : α) (p : a ≈ b),
      ⋯ ▸ f a = f b)
  (q : Quotient s) : motive q

针对 Quotient 的依值递归原理。它类似于结构体的对鬼子，可以用于当结果类型不一定是命题时的情况。

虽然此递归子非常通用，但实际使用时可能较为棘手。以下几种更简单的选取，可能更容易上手：

Quotient.lift 适用于定义非依值（非依赖）函数。
Quotient.ind 适用于证明关于商集的定理。
每当目标类型是 Subsingleton（子单元）时，可以使用 Quotient.recOnSubsingleton。
Quotient.hrecOn 使用异质等价（heterogeneous equality），而非通过 Quotient.sound 进行重写。

Quotient.recOn 是该递归子的一个版本，它首先接收商集参数。

def

Quotient.recOn.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v} (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) : motive q
Quotient.recOn.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (h :
    ∀ (a b : α) (p : a ≈ b),
      ⋯ ▸ f a = f b) :
  motive q

一个用于 Quotient 的依值递归原理（dependent recursion principle）。它类似于结构体的递归子，当结果类型不一定是命题时，可以使用它。

尽管这个递归子非常通用，但实际使用上可能较为棘手。以下这些更简单的选项通常更易于使用：

Quotient.lift 适合定义非依值函数。
Quotient.ind 适合用于对商类型证明定理。
每当目标类型为 {tech key := "subsingleton"}[子单元] 时，可以使用 Quotient.recOnSubsingleton。
Quotient.hrecOn 使用异质等价，而不是通过 Quotient.sound 进行重写。

Quotient.rec 是该递归子的一个变体，不同之处在于它将商类型参数放在最后。

def

Quotient.hrecOn.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v} (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (c : ∀ (a b : α), a ≈ b → f a ≍ f b) : motive q
Quotient.hrecOn.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (c : ∀ (a b : α), a ≈ b → f a ≍ f b) :
  motive q

Quotient 的一个依值递归原理（dependent recursion principle），它利用了异质等价（见 HEq），类似于结构体的递归子。

Quotient.recOn 是这个递归子的一个版本，不过它用的是 Eq 而不是 HEq。

若某类型的两个元素在某商类型中相等，则它们在集合体等价关系下也等价。这个性质叫做 Quotient.exact。

theorem

Quotient.exact.{u} {α : Sort u} {s : Setoid α} {a b : α} :
  Quotient.mk s a = Quotient.mk s b → a ≈ b
Quotient.exact.{u} {α : Sort u}
  {s : Setoid α} {a b : α} :
  Quotient.mk s a = Quotient.mk s b →
    a ≈ b

如果两个值在商类型中是相等的，那么它们必定满足该商类型的等价关系。

4.5.5. 逻辑模型🔗

类似函数和宇宙，商类型是 Lean 类型系统的内建特性。但底层原语是基于更简单的 Quot 类型，而不是 Quotient，后者是基于前者实现的。主要区别在于 Quot 可以接受任意关系，并不限于 Setoid 实例。而且提供的关系不必先是等价关系。Quot 和 Eq 的相关规则自动向外扩展为自反、传递和对称。如果用的是等价关系，应优先选用 Quotient 以便 Lean 利用更多性质。

最基本的商类型操作有 Quot，Quot.mk，Quot.lift，Quot.ind，Quot.sound。它们的用法与对应的基于 Quotient 的 API 类似。

primitive

Quot.{u} {α : Sort u} (r : α → α → Prop) : Sort u
Quot.{u} {α : Sort u} (r : α → α → Prop) :
  Sort u

底层商类型。商类型将类型 α 的命题等价关系加以粗化，使得由某个关系 r 相关联的项在 Quot r 中被视为相等。

从集合论的角度来看，Quot r 可以看作是在 r 下将 α 划分同余类所形成的集合。想要从 Quot r 构造函数，必须证明该函数保持关系 r：如果要定义 f : Quot r → β，需要给出 f' : α → β，并证明对于所有 x : α 和 y : α，若 r x y，则 f' x = f' y。

Quot 是一个内建的原语类型：

Quot.mk 用于把基础类型 α 的元素放入商类型中。
Quot.lift 用于定义从商类型到其他类型的函数。
Quot.sound 用于断言由关系 r 关联的元素相等。
Quot.ind 支持基于假设所有元素都是由 Quot.mk 构造，进行关于商类型的证明。

关系 r 并不要求一定是等价关系；由等价和商类型的规则可知，最终得到的商类型的等价性会将 r 延伸为等价关系。当 r 本身就是等价关系时，推荐使用更高级的 Quotient 类型，这样会更便捷。

primitive

Quot.mk.{u} {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
Quot.mk.{u} {α : Sort u}
  (r : α → α → Prop) (a : α) : Quot r

将某一类型的元素放置在一个等价类中，该等价类根据给定的关系将项等同起来。

给定 v : α 和关系 r : α → α → Prop，Quot.mk r v : Quot r 相当于 v，只是对 v 值的所有观察都必须遵守关系 r。

Quot.mk 是内建的原语：

Quot 是内建的商类型。
Quot.lift 允许从商类型定义到其他类型的函数。
Quot.sound 断言所有被关系 r 关联的元素的相等性。
Quot.ind 用于写关于商类型的证明，该证明假设所有元素都由 Quot.mk 构造。

primitive

Quot.lift.{u, v} {α : Sort u} {r : α → α → Prop} {β : Sort v}
  (f : α → β) (a : ∀ (a b : α), r a b → f a = f b) : Quot r → β
Quot.lift.{u, v} {α : Sort u}
  {r : α → α → Prop} {β : Sort v}
  (f : α → β)
  (a : ∀ (a b : α), r a b → f a = f b) :
  Quot r → β

将一个函数从基础类型提升到商类型上的函数时，要求该函数满足商的关系约束。

对于一个关系 r : α → α → Prop 和商类型 Quot r，如果想要应用函数 f : α → β，则还需提供一个证明 a，用于保证 f 满足关系 r。此时，Quot.lift f a : Quot r → β 得到的值与直接用 f 计算一致。

Lean 的类型理论中包含一个定义性规约，将 Quot.lift f h (Quot.mk r v) 规约为 f v。

Quot.lift 是一个内建原语：

Quot 是内建的商类型。
Quot.mk 用于将基础类型 α 的元素放入商类型中。
Quot.sound 用于断言因 r 相关的两个元素相等。
Quot.ind 用于针对商类型进行证明，此时可以假设所有元素都是用 Quot.mk 构造的；它的作用类似于结构体的递归子。

primitive

Quot.ind.{u} {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
  (mk : ∀ (a : α), β (Quot.mk r a)) (q : Quot r) : β q
Quot.ind.{u} {α : Sort u}
  {r : α → α → Prop} {β : Quot r → Prop}
  (mk : ∀ (a : α), β (Quot.mk r a))
  (q : Quot r) : β q

一个用于商类型（quotients）的推理原则，它允许在关于商类型的证明中假定所有的值都是由 Quot.mk 构造的。

Quot.rec 类似于结构体的递归子，当结果类型不一定是命题时可以使用它。

Quot.ind 是一个内置的原语：

Quot 是内置的商类型。
Quot.mk 用于将底层类型 α 的元素放入商类型中。
Quot.lift 允许从商类型到其他类型的函数定义。
Quot.sound 断言了被关系 r 关联的元素的相等性。

axiom

Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} :
  r a b → Quot.mk r a = Quot.mk r b
Quot.sound.{u} {α : Sort u}
  {r : α → α → Prop} {a b : α} :
  r a b → Quot.mk r a = Quot.mk r b

商公理，断言由商集合的关系所联系的元素是相等的。

关系 r 并不需要是等价关系才能使用此公理。当 r 不是等价关系时，商集是关于由 r 生成的等价关系而言的。

Quot.sound 是内置原语型商类型的一部分：

Quot 是内置的商类型。
Quot.mk 用于将底层类型 α 的元素放入商集中。
Quot.lift 允许定义从商类型到其他类型的函数。
Quot.ind 用于在证明与商类型有关的命题时进行归纳，方法是假设所有元素都是通过 Quot.mk 构造的；它类似于结构体的递归子。

关于商类型的更详细描述见 Lean 语言参考手册。

4.5.5.1. 商类型规约🔗

除了上述常量之外，Lean 的内核还包含了关于 Quot.lift 的规约规则，使其在与 Quot.mk 一起使用时能够规约，这类似于归纳类型的 ι-规约。给定在 α 上的一个关系 r，一个从 α 到 β 的函数 f，以及一个证明 resp，表明 f 保持了 r，那么项 Quot.lift f resp (Quot.mk r x) 与 f x 是定义等价的。

variable
  (r : α → α → Prop)
  (f : α → β)
  (ok : ∀ x y, r x y → f x = f y)
  (x : α)

example : Quot.lift f ok (Quot.mk r x) = f x := rfl

4.5.5.2. 商类型与归纳类型🔗

由于 Quot 不是归纳类型，因此作为商类型实现的类型不能作为嵌套项出现在归纳类型定义中。此时需拆解商类型，将归纳类型定义为无商版本，再对其定义独立的等价关系。

嵌套归纳类型与商类型

RoseTree的嵌套归纳类型，是将递归出现的 RoseTree 嵌套在 List 之下：

inductive RoseTree (α : Type u) where
  | leaf : α → RoseTree α
  | branch : List (RoseTree α) → RoseTree α

然而，对 List 按照压缩类型的方式，将所有元素视为相同来取商会导致 Lean 拒绝该声明：

(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declaredinductive SetTree (α : Type u) where
  | leaf : α → SetTree α
  | branch :
    Quot (fun (xs ys : List (SetTree α)) => True) →
    SetTree α

(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declared

Quot.liftOn 是 Quot.lift 的变体，将商类型值放参数首，与 Quotient.liftOn 类似。

def

Quot.liftOn.{u, v} {α : Sort u} {β : Sort v} {r : α → α → Prop}
  (q : Quot r) (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) : β
Quot.liftOn.{u, v} {α : Sort u}
  {β : Sort v} {r : α → α → Prop}
  (q : Quot r) (f : α → β)
  (c : ∀ (a b : α), r a b → f a = f b) : β

将某个函数从底层类型提升为商类型上的函数，前提是该函数要满足商类型上的等价关系。

假设有一个关系 r : α → α → Prop，以及商类型中的一个值 q : Quot r，若要对其应用函数 f : α → β，则需要提供一个证明 c，说明 f 能够保持（即满足）关系 r。在这种情况下，Quot.liftOn q f h : β 的计算结果是将 f 应用于 q 所对应的底层 α 类型的值后所得的结果。

Quot.liftOn 是内建原语 Quot.lift 的一个参数顺序重新排列后的版本。

关于商类型的更多细节，可以参考 Lean 语言参考文档的对应章节。

Lean 还提供了从 Quot 到任意子单元的消解，无需额外证明，以及与 Quotient 相对应的依赖消解原理。

def

Quot.recOnSubsingleton.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v}
  [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a)) : motive q
Quot.recOnSubsingleton.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v}
  [h :
    ∀ (a : α),
      Subsingleton (motive (Quot.mk r a))]
  (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a)) :
  motive q

当目标类型是一个子单元时，可以使用这种选取的归纳原理来处理商类型。

在这种情况下，函数满足商类型关系的证明是平凡的，因此任何函数都可以被提升。

Quot.rec 并不假设目标类型为子单元。

def

Quot.rec.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a))
  (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (q : Quot r) : motive q
Quot.rec.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v}
  (f : (a : α) → motive (Quot.mk r a))
  (h :
    ∀ (a b : α) (p : r a b),
      ⋯ ▸ f a = f b)
  (q : Quot r) : motive q

Quot 的依值递归原理。它类似于结构体的递归子，当结果类型不一定是命题时可以使用。

虽然这种递归子极为通用，但有时使用起来不太方便。以下这些更简单的选项可能更易于使用：

Quot.lift 适用于定义非依值的函数。
Quot.ind 适用于证明关于商类型的定理。
只要目标类型是一个 Subsingleton（子单元），就可以使用 Quot.recOnSubsingleton。
Quot.hrecOn 使用了 {tech key := "heterogeneous equality"}[异质等价]，而不是用 Quot.sound 进行重写。

Quot.recOn 是该递归子的一种变体，它首先传入商类型参数。

def

Quot.recOn.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) : motive q
Quot.recOn.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (h :
    ∀ (a b : α) (p : r a b),
      ⋯ ▸ f a = f b) :
  motive q

Quot 的依值递归原理。它类似于结构体的递归子，当结果类型不一定是命题时可以使用。

虽然这种递归子极为通用，但有时使用起来不太方便。以下这些更简单的选项可能更易于使用：

Quot.lift 适用于定义非依值的函数。
Quot.ind 适用于证明关于商类型的定理。
只要目标类型是一个 Subsingleton（子单元），就可以使用 Quot.recOnSubsingleton。
Quot.hrecOn 使用了 {tech key := "heterogeneous equality"}[异质等价]，而不是用 Quot.sound 进行重写。

Quot.recOn 是该递归子的一种变体，它首先传入商类型参数。

def

Quot.hrecOn.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (c : ∀ (a b : α), r a b → f a ≍ f b) : motive q
Quot.hrecOn.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (c : ∀ (a b : α), r a b → f a ≍ f b) :
  motive q

Quot 的依值递归原理（recursion principle），它使用了异质等价，类似于结构体的递归子。

Quot.recOn 是一个类似的递归子，它使用 Eq 替代了 HEq。

4.5.6. 商类型与函数外延性🔗

由于 Lean 的定义等价包含了 Quot.lift 的计算规约规则，标准库中用商类型来证明函数外延性，否则这个结果通常需要作为一个公理引入。具体做法是，先定义一种按外延等价关系取商的函数类型，对于这种类型，外延等价是定义成立的。

variable {α : Sort u} {β : α → Sort v}

def extEq (f g : (x : α) → β x) : Prop :=
  ∀ x, f x = g x

def ExtFun (α : Sort u) (β : α → Sort v) :=
  Quot (@extEq α β)

外延函数和普通函数一样可以调用。函数应用本身就满足外延等价：只要对所有输入应用得到的结果都相等，那应用后的结果自然也相等。

def extApp
    (f : ExtFun α β)
    (x : α) :
    β x :=
  f.lift (· x) fun g g' h => byα:Sort uβ:α → Sort vf:ExtFun α βx:αg:(x : α) → β xg':(x : α) → β xh:extEq g g'⊢ (fun x_1 => x_1 x) g = (fun x_1 => x_1 x) g'
    exact h xAll goals completed! 🐙

为了证明两个函数在外延意义下相等就等价于本身相等，只需证明它们各自转换为外延函数之后，再通过外延化应用的方法得到的结果是相等的。原因在于

extApp (Quot.mk _ f)

在定义上等价于

fun x => (Quot.mk extEq f).lift (· x) (fun _ _ h => h x)

定义上等价于 fun x => f x，而根据 η-等价，又等价于 f。如果 Quot.lift 的计算规则只是命题形式，而不是定义等价的形式，那就不满足，因为规约表达式会出现在函数体里，按等式重写一整个函数本身就需要函数外延性。

于是，只要证明参与两端的外延版函数真的相等即可。这正是由于 Quot.sound 成立：即它们本就在商类型的等价关系下。这里的证明其实比标准库里的写法更为直白：

theorem funext'
    {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) :
    f = g := byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ f = g
  suffices extApp (Quot.mk _ f) = extApp (Quot.mk _ g) byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:extApp (Quot.mk extEq f) = extApp (Quot.mk extEq g)⊢ f = g
    unfold extApp at thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:(fun x => Quot.lift (fun x_1 => x_1 x) ⋯ (Quot.mk extEq f)) = fun x => Quot.lift (fun x_1 => x_1 x) ⋯ (Quot.mk extEq g)⊢ f = g
    dsimp at thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:(fun x => f x) = fun x => g x⊢ f = g
    exact thisAll goals completed! 🐙
  suffices Quot.mk extEq f = Quot.mk extEq g byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:Quot.mk extEq f = Quot.mk extEq g⊢ extApp (Quot.mk extEq f) = extApp (Quot.mk extEq g)
    apply congrArghα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:Quot.mk extEq f = Quot.mk extEq g⊢ Quot.mk extEq f = Quot.mk extEq g
    exact thisAll goals completed! 🐙
  apply Quot.soundaα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ extEq f g
  exact hAll goals completed! 🐙

4.5.7. 压缩类型🔗

压缩类型（Squash types）是以“所有元素互相关联”的关系取商后的类型，这样得到的就是一个子单元。换句话说，如果 α 中有元素，那么 Squash α 就只有一个元素；如果 α 为空，则 Squash α 也为空。和 Nonempty α 不同，后者只是一个“α 非空”这一命题，在运行时只表现为一个占位值；而 Squash α 是类型层面的，它在表示层和 α 完全一样。并且由于 Squash α 和 α 处在同一个宇宙层级，它不受“不能从命题中计算数据”的限制。

def

Squash.{u} (α : Sort u) : Sort u
Squash.{u} (α : Sort u) : Sort u

α 关于全体关系的商。Squash α 的元素就是 α 的元素，但它们在此被视为全都相等，无法区分。

Squash α 是一个子单元：若 α 为空，则 Squash α 也为空；否则只有一个元素。它可以看作是从 α 映射来的“通用子单元”。

Nonempty α 同样拥有这些性质。它是一个命题，也就是说它的元素（比如: 证明）在编译代码时会被抹去，只用一个占位值表示。而 Squash α 是 Type u，且它在编译代码中的表现形式和 α 相同。

因此，Squash.lift 可以将一个 α 的值提取到任何子单元类型 β 中，而 Nonempty.rec 只能在 β 是命题时才能做同样的事情。

def

Squash.mk.{u} {α : Sort u} (x : α) : Squash α
Squash.mk.{u} {α : Sort u} (x : α) :
  Squash α

将一个值放入其 squash 类型中，在该类型中它无法与其他任何值区分。

def

Squash.lift.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} [Subsingleton β]
  (s : Squash α) (f : α → β) : β
Squash.lift.{u_1, u_2} {α : Sort u_1}
  {β : Sort u_2} [Subsingleton β]
  (s : Squash α) (f : α → β) : β

从压缩值中提取为任意子单元类型。

如果 β 是一个子单元类型，则函数 α → β 无法区分 α 的各个元素，因此自动满足 Squash 所等价化的普遍关系。

theorem

Squash.ind.{u} {α : Sort u} {motive : Squash α → Prop}
  (h : ∀ (a : α), motive (Squash.mk a)) (q : Squash α) : motive q
Squash.ind.{u} {α : Sort u}
  {motive : Squash α → Prop}
  (h : ∀ (a : α), motive (Squash.mk a))
  (q : Squash α) : motive q

一种推理原则，它允许在证明关于 squash 类型时，假定所有的值都是通过 Squash.mk 构造出来的。

4.5. 商类型🔗

4.5.1. 商类型的替代方案🔗

4.5.2. 集合体 （Setoid）🔗

Instance Constructor

Methods

4.5.3. 等价关系🔗

Instance Constructor

Methods

Constructor

Fields

4.5.4. 商类型 API🔗

4.5.4.1. 构造商类型🔗

4.5.4.2. 消解商类型🔗

4.5.4.3. 商类型上的证明🔗

4.5.5. 逻辑模型🔗

4.5.5.1. 商类型规约🔗

4.5.5.2. 商类型与归纳类型🔗

4.5.6. 商类型与函数外延性🔗

4.5.7. 压缩类型🔗

4.5.2. 集合体（Setoid）🔗